翻訳と辞書 Words near each other ・ Resource (band) ・ Resource (biology) ・ Resolution independence ・ Resolution inference ・ Resolution Island ・ Resolution Island (New Zealand) ・ Resolution Island (Nunavut) ・ Resolution of Sarajevo Muslims ・ Resolution of singularities ・ Resolution of the Comintern on the Macedonian Question ・ Resolution of the Dreyfus Affair ・ Resolution on Taiwan's Future ・ Resolution Party ・ Resolution plc ・ Resolution Point ・ Resolution proof compression by splitting ・ Resolution proof reduction via local context rewriting ・ Resolution Rupes ・ Resolution Subglacial Highlands ・ Resolution Tour ・ Resolution Trust Corporation ・ Resolution, U.S. Virgin Islands ・ Resolution-class submarine ・ Resolutions (album) ・ Resolutions of the Flemish Parliament of 1999 ・ Resolutions of the United Church of Christ ・ Resolv.conf ・ Resolvability criterion ・ Resolvable space ・ Resolvconf Dictionary Lists mini英和辞書 mini和英辞書 Webster 1913 Latin-English FOLDOC Wikipedia English ウィキペディア

翻訳と辞書　辞書検索 [ 開発暫定版 ] スポンサード リンク Resolution proof compression by splitting ： ウィキペディア英語版 Resolution proof compression by splitting In mathematical logic, proof compression by splitting is an algorithm that operates as a post-process on resolution proofs. It was proposed by Scott Cotton in his paper "Two Techniques for Minimizing Resolution Proof".〔Cotton, Scott. "Two Techniques for Minimizing Resolution Proofs". 13th International Conference on Theory and Applications of Satisfiability Testing, 2010.〕 The Splitting algorithm is based on the following observation: Given a proof of unsatisfiability $\backslash pi$ and a variable $x$, it is easy to re-arrange (split) the proof in a proof of $x$ and a proof of $\backslash neg\; x\; \backslash !$ and the recombination of these two proofs (by an additional resolution step) may result in a proof smaller than the original. Note that applying Splitting in a proof $\backslash pi$ using a variable $x$ does not invalidates a latter application of the algorithm using a differente variable $y$. Actually, the method proposed by Cotton〔 generates a sequence of proofs $\backslash pi\_1\; \backslash pi\_2\; \backslash ldots$, where each proof $\backslash pi\_$ is the result of applying Splitting to $\backslash pi\_i$. During the construction of the sequence, if a proof $\backslash pi\_j$ happens to be too large, $\backslash pi\_$ is set to be the smallest proof in $\backslash$. For achieving a better compression/time ratio, a heuristic for variable selection is desirable. For this purpose, Cotton〔 defines the "additivity" of a resolution step (with antecedents $p$ and $n$ and resolvent $r$): : $\backslash operatorname(r)\; :=\; \backslash max(|r|-\backslash max(|p|,\; |n|),\; 0)\; \backslash ,$ Then, for each variable $v$, a score is calculated summing the additivity of all the resolution steps in $\backslash pi$ with pivot $v$ together with the number of these resolution steps. Denoting each score calculated this way by $add(v,\; \backslash pi)$, each variable is selected with a probability proportional to its score: : $p(v)\; =\; \backslash frac\}$ To split a proof of unsatisfiability $\backslash pi$ in a proof $\backslash pi\_x$ of $x$ and a proof $\backslash pi\_$ of $\backslash neg\; x$, Cotton 〔 proposes the following: Let $l$ denote a literal and $p\; \backslash oplus\; \_x\; n$ denote the resolvent of clauses $p$ and $n$ where $x\; \backslash in\; p$ and $\backslash neg\; x\; \backslash in\; n$. Then, define the map $\backslash pi\_l$ on nodes in the resolution dag of $\backslash pi$: :$\backslash pi\_l(c)\; :=\; \backslash begin$ c, & \text c \text \\ \pi_l(p), & \text c = p \oplus_x n \text (l = x \text x \notin \pi_l(p)) \\ \pi_l(n), & \text c = p \oplus_x n \text (l = \neg x \mbox \neg x \notin \pi_l(n)) \\ \pi_l(p) \oplus_x \pi_l(p), & \text x \in \pi_l(p) \text \neg x \in \pi_l(n) \end Also, let $o$ be the empty clause in $\backslash pi$. Then, $\backslash pi\_x$ and $\backslash pi\_$ are obtained by computing $\backslash pi\_x(o)$ and $\backslash pi\_(o)$, respectively. == Notes == 抄文引用元・出典: フリー百科事典『 ウィキペディア（Wikipedia）』 ■ウィキペディアで「Resolution proof compression by splitting」の詳細全文を読む スポンサード リンク 翻訳と辞書 : 翻訳のためのインターネットリソース Copyright(C) kotoba.ne.jp 1997-2016. All Rights Reserved.